import java.io.PrintStream;
import java.io.PrintWriter;
import java.io.StringWriter;
import java.text.DecimalFormat;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.Properties;

import edu.ksu.cis.projects.bogor.Bogor;
import edu.ksu.cis.projects.bogor.DefaultBogorConfiguration;
import edu.ksu.cis.projects.bogor.IBogorConfiguration;
import edu.ksu.cis.projects.bogor.module.IMessageStore;
import edu.ksu.cis.projects.bogor.module.IProgressManager;
import edu.ksu.cis.projects.bogor.module.ISchedulingStrategyContext;
import edu.ksu.cis.projects.bogor.module.ISchedulingStrategyInfo;
import edu.ksu.cis.projects.bogor.module.ISearcher;
import edu.ksu.cis.projects.bogor.module.IStateManager;
import edu.ksu.cis.projects.bogor.module.backtrack.IExceptionBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.ITransformationBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.config.ISelfDescribingModule;
import edu.ksu.cis.projects.bogor.module.throwable.AssertionBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.BogorException;
import edu.ksu.cis.projects.bogor.module.throwable.ExceptionThrownBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.ExtFailedBogorException;
import edu.ksu.cis.projects.bogor.module.throwable.RangeBogorException;
import edu.ksu.cis.projects.bogor.module.value.IIntValue;
import edu.ksu.cis.projects.bogor.module.value.IValue;
import edu.ksu.cis.projects.bogor.symboltable.SymbolTable;
import edu.ksu.cis.projects.bogor.util.Util;
import edu.ksu.cis.projects.bogor.ast.System;


public class Searcher {

	private PrintWriter pw;
	private int currentDepth;
	private int maxDepth = 50;
	private boolean allAsErrors = false;
	private int errors;
	protected ISearcher sr;
	protected int maxErrors;
	protected int stateId;
	private int currentMaxDepth;
	protected int invisibleMoves;
	protected IStateManager sm;
	
	public Searcher(){
		init();
	}
	
	private void init(){
		StringWriter sw = new StringWriter();
	    this.pw = new PrintWriter(sw);
	}

	public void test(System model){
		SymbolTable symbolTable = new SymbolTable("wxqtest", model);
		
//		IMessageStore messageStore = Bogor.modelCheck(symbolTable, this.pw, null /*this.progressManager*/,  new DefaultBogorConfiguration(), null/*configuration*/, );
		
		IBogorConfiguration bc = new DefaultBogorConfiguration();
		bc.initialize(symbolTable, null, pw, new Properties(), new HashMap());
		ISearcher searcher = bc.getSearcher();
		searcher.initialize();
	    bc.getSearcher().search();
	}

}

class MaxErrorReachedException extends RuntimeException {
}